es:ES, ds:x:Id fp Type, T:Type, i:Id, f:(State(ds)T).
(x, y:T. Dec(x = y))
 @i discrete ds
 e'@i.
 (e<e'. f((discrete state when e)) = f((discrete state when e')))
  (e:E
  (((e <loc e')
  (c (((f((discrete state when e)) = f((discrete state after e))))
  (c & (e'':E.
  (c & ((e <loc e'')
  (c & ( e'' loc e' 
  (c & ( (f((discrete state when e'')) = f((discrete state when e'))  T))))) 

latex

Definitions

x. t(x), t  T, , e loc e' , P & Q, (e <loc e'), A c B, x:A. B(x), P  Q, e@i. P(e), P  Q, x:A. B(x), e<e'. P(e), True, T, {T}, A, discrete state@i, State(ds), P  Q, SQType(T), x(s), P  Q, False, Dec(P)

Lemmas

event system wf, fpf wf, Id wf, decl-state wf, decidable wf, es-dds wf, es-first wf, assert wf, es-le-loc, es-locl wf, es-dstate-after wf, es-locl-iff, es-loc-pred, not wf, es-causl wf, Id sq, es-dstate-subtype, es-dstate-when wf, es-loc wf, alle-lt wf, alle-at-iff, es-le wf, es-E wf, true wf, squash wf, es-le weakening, es-locl transitivity2, es-pred-locl, es-le-iff, dstate-after-pred, equal functionality wrt subtype rel, id-deq wf, fpf-cap wf, top wf, es-vartype wf, es-isconst wf, ifthenelse wf, es-axioms